Nuprl Lemma : non_nil_length
11,40
postcript
pdf
T
:Type,
L
:(
T
List). (
(
L
= []))
(0 < ||
L
||)
latex
Definitions
prop{i:l}
,
t
T
,
Y
,
||
as
||
,
P
Q
,
x
:
A
.
B
(
x
)
,
False
,
A
Lemmas
non
neg
length
,
length
wf1
,
not
wf
origin
T:Type, L:(T List). (
(L = [])) 
(0 < ||L||) T:Type, L:(T List). ((L = [])) (0 < ||L||) 
T Qx:A. B(x)A